Termination Proof Script
Consider the TRS R consisting of the rewrite rules
|
| 1: |
|
x : x |
→ e |
| 2: |
|
x : e |
→ x |
| 3: |
|
i(x : y) |
→ y : x |
| 4: |
|
(x : y) : z |
→ x : (z : i(y)) |
| 5: |
|
e : x |
→ i(x) |
| 6: |
|
i(i(x)) |
→ x |
| 7: |
|
i(e) |
→ e |
| 8: |
|
x : (y : i(x)) |
→ i(y) |
| 9: |
|
x : (y : (i(x) : z)) |
→ i(z) : y |
| 10: |
|
i(x) : (y : x) |
→ i(y) |
| 11: |
|
i(x) : (y : (x : z)) |
→ i(z) : y |
|
There are 11 dependency pairs:
|
| 12: |
|
I(x : y) |
→ y :# x |
| 13: |
|
(x : y) :# z |
→ x :# (z : i(y)) |
| 14: |
|
(x : y) :# z |
→ z :# i(y) |
| 15: |
|
(x : y) :# z |
→ I(y) |
| 16: |
|
e :# x |
→ I(x) |
| 17: |
|
x :# (y : i(x)) |
→ I(y) |
| 18: |
|
x :# (y : (i(x) : z)) |
→ i(z) :# y |
| 19: |
|
x :# (y : (i(x) : z)) |
→ I(z) |
| 20: |
|
i(x) :# (y : x) |
→ I(y) |
| 21: |
|
i(x) :# (y : (x : z)) |
→ i(z) :# y |
| 22: |
|
i(x) :# (y : (x : z)) |
→ I(z) |
|
Consider the SCC {12-22}.
The constraints could not be solved.
Tyrolean Termination Tool (0.05 seconds)
--- May 4, 2006